$\forall$$M$:MsgA, $l$:IdLnk, ${\it mss}$:$M$.Msg List. withlnk($l$;${\it mss}$) $\in$ (${\it tg}$:Id$\times$$M$.dout($l$,${\it tg}$)) List